Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/nonlinear_extension.cpp	Lines:	291	325	89.5 %
Date:	2021-08-14	Branches:	489	965	50.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "theory/arith/nl/nonlinear_extension.h"

#include "options/arith_options.h"
#include "theory/arith/arith_state.h"
#include "theory/arith/bound_inference.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/arith/theory_arith.h"
#include "theory/ext_theory.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
#include "util/rational.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace arith {
namespace nl {

NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                       ArithState& state,
                                       eq::EqualityEngine* ee,
                                       ProofNodeManager* pnm)
    : d_containing(containing),
      d_im(containing.getInferenceManager()),
      d_needsLastCall(false),
      d_checkCounter(0),
      d_extTheoryCb(ee),
      d_extTheory(d_extTheoryCb,
                  containing.getSatContext(),
                  containing.getUserContext(),
                  containing.getOutputChannel()),
      d_model(containing.getSatContext()),
      d_trSlv(d_im, d_model, pnm, containing.getUserContext()),
      d_extState(d_im, d_model, pnm, containing.getUserContext()),
      d_factoringSlv(&d_extState),
      d_monomialBoundsSlv(&d_extState),
      d_monomialSlv(&d_extState),
      d_splitZeroSlv(&d_extState),
      d_tangentPlaneSlv(&d_extState),
      d_cadSlv(d_im, d_model, state.getUserContext(), pnm),
      d_icpSlv(d_im),
      d_iandSlv(d_im, state, d_model),
      d_pow2Slv(d_im, state, d_model)
{
  d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
  d_extTheory.addFunctionKind(kind::EXPONENTIAL);
  d_extTheory.addFunctionKind(kind::SINE);
  d_extTheory.addFunctionKind(kind::PI);
  d_extTheory.addFunctionKind(kind::IAND);
  d_extTheory.addFunctionKind(kind::POW2);
  d_true = NodeManager::currentNM()->mkConst(true);
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
  d_one = NodeManager::currentNM()->mkConst(Rational(1));
  d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));

  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
  if (pc != nullptr)
  {
    d_proofChecker.registerTo(pc);
  }
}

NonlinearExtension::~NonlinearExtension() {}

void NonlinearExtension::preRegisterTerm(TNode n)
{
  // register terms with extended theory, to find extended terms that can be
  // eliminated by context-depedendent simplification.
  d_extTheory.registerTerm(n);
}

void NonlinearExtension::processSideEffect(const NlLemma& se)
{
  d_trSlv.processSideEffect(se);
}

void NonlinearExtension::computeRelevantAssertions(
    const std::vector<Node>& assertions, std::vector<Node>& keep)
{
  Trace("nl-ext-rlv") << "Compute relevant assertions..." << std::endl;
  Valuation v = d_containing.getValuation();
  for (const Node& a : assertions)
  {
    if (v.isRelevant(a))
    {
      keep.push_back(a);
    }
  }
  Trace("nl-ext-rlv") << "...keep " << keep.size() << "/" << assertions.size()
                      << " assertions" << std::endl;
}

void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
{
  Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl;
  bool useRelevance = false;
  if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE)
  {
    useRelevance = (d_checkCounter % 2);
  }
  else if (options::nlRlvMode() == options::NlRlvMode::ALWAYS)
  {
    useRelevance = true;
  }
  Valuation v = d_containing.getValuation();

  BoundInference bounds;

  std::unordered_set<Node> init_assertions;

  for (Theory::assertions_iterator it = d_containing.facts_begin();
       it != d_containing.facts_end();
       ++it)
  {
    const Assertion& assertion = *it;
    Trace("nl-ext-assert-debug")
        << "Loaded " << assertion.d_assertion << " from theory" << std::endl;
    Node lit = assertion.d_assertion;
    if (useRelevance && !v.isRelevant(lit))
    {
      // not relevant, skip
      continue;
    }
    if (bounds.add(lit, false))
    {
      continue;
    }
    init_assertions.insert(lit);
  }

  for (const auto& vb : bounds.get())
  {
    const Bounds& b = vb.second;
    if (!b.lower_bound.isNull())
    {
      init_assertions.insert(b.lower_bound);
    }
    if (!b.upper_bound.isNull())
    {
      init_assertions.insert(b.upper_bound);
    }
  }

  // Try to be "more deterministic" by adding assertions in the order they were
  // given
  for (auto it = d_containing.facts_begin(); it != d_containing.facts_end();
       ++it)
  {
    Node lit = (*it).d_assertion;
    auto iait = init_assertions.find(lit);
    if (iait != init_assertions.end())
    {
      Trace("nl-ext-assert-debug") << "Adding " << lit << std::endl;
      assertions.push_back(lit);
      init_assertions.erase(iait);
    }
  }
  // Now add left over assertions that have been newly created within this
  // function by the code above.
  for (const Node& a : init_assertions)
  {
    Trace("nl-ext-assert-debug") << "Adding " << a << std::endl;
    assertions.push_back(a);
  }
  Trace("nl-ext") << "...keep " << assertions.size() << " / "
                  << d_containing.numAssertions() << " assertions."
                  << std::endl;
}

std::vector<Node> NonlinearExtension::checkModelEval(
    const std::vector<Node>& assertions)
{
  std::vector<Node> false_asserts;
  for (size_t i = 0; i < assertions.size(); ++i)
  {
    Node lit = assertions[i];
    Node atom = lit.getKind() == NOT ? lit[0] : lit;
    Node litv = d_model.computeConcreteModelValue(lit);
    Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv;
    if (litv != d_true)
    {
      Trace("nl-ext-mv-assert") << " [model-false]" << std::endl;
      false_asserts.push_back(lit);
    }
    else
    {
      Trace("nl-ext-mv-assert") << std::endl;
    }
  }
  return false_asserts;
}

bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
{
  Trace("nl-ext-cm") << "--- check-model ---" << std::endl;

  // get the presubstitution
  Trace("nl-ext-cm-debug") << "  apply pre-substitution..." << std::endl;
  // Notice that we do not consider relevance here, since assertions were
  // already filtered based on relevance. It is incorrect to filter based on
  // relevance here, since we may have discarded literals that are relevant
  // that are entailed based on the techniques in getAssertions.
  std::vector<Node> passertions = assertions;
  if (options::nlExt() == options::NlExtMode::FULL)
  {
    // preprocess the assertions with the trancendental solver
    if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
    {
      return false;
    }
  }
  if (options::nlCad())
  {
    d_cadSlv.constructModelIfAvailable(passertions);
  }

  Trace("nl-ext-cm") << "-----" << std::endl;
  unsigned tdegree = d_trSlv.getTaylorDegree();
  std::vector<NlLemma> lemmas;
  bool ret = d_model.checkModel(passertions, tdegree, lemmas);
  for (const auto& al: lemmas)
  {
    d_im.addPendingLemma(al);
  }
  return ret;
}

void NonlinearExtension::check(Theory::Effort e)
{
  d_im.reset();
  Trace("nl-ext") << std::endl;
  Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl;
  if (e == Theory::EFFORT_FULL)
  {
    d_needsLastCall = true;
    if (options::nlExtRewrites())
    {
      std::vector<Node> nred;
      if (!d_extTheory.doInferences(0, nred))
      {
        Trace("nl-ext") << "...sent no lemmas, # extf to reduce = "
                        << nred.size() << std::endl;
        if (nred.empty())
        {
          d_needsLastCall = false;
        }
      }
      else
      {
        Trace("nl-ext") << "...sent lemmas." << std::endl;
      }
    }
  }
  else
  {
    // If we computed lemmas during collectModelInfo, send them now.
    if (d_im.hasPendingLemma())
    {
      d_im.doPendingFacts();
      d_im.doPendingLemmas();
      d_im.doPendingPhaseRequirements();
      return;
    }
    // Otherwise, we will answer SAT. The values that we approximated are
    // recorded as approximations here.
    TheoryModel* tm = d_containing.getValuation().getModel();
    for (std::pair<const Node, std::pair<Node, Node>>& a : d_approximations)
    {
      if (a.second.second.isNull())
      {
        tm->recordApproximation(a.first, a.second.first);
      }
      else
      {
        tm->recordApproximation(a.first, a.second.first, a.second.second);
      }
    }
    for (const auto& vw : d_witnesses)
    {
      tm->recordApproximation(vw.first, vw.second);
    }
  }
}

Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
{
  ++(d_stats.d_mbrRuns);
  d_checkCounter++;

  // get the assertions
  std::vector<Node> assertions;
  getAssertions(assertions);

  Trace("nl-ext-mv-assert")
      << "Getting model values... check for [model-false]" << std::endl;
  // get the assertions that are false in the model
  const std::vector<Node> false_asserts = checkModelEval(assertions);
  Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl;

  // get the extended terms belonging to this theory
  std::vector<Node> xtsAll;
  d_extTheory.getTerms(xtsAll);
  // only consider those that are currently relevant based on the current
  // assertions, i.e. those contained in termSet
  std::vector<Node> xts;
  for (const Node& x : xtsAll)
  {
    if (termSet.find(x) != termSet.end())
    {
      xts.push_back(x);
    }
  }

  if (Trace.isOn("nl-ext-debug"))
  {
    Trace("nl-ext-debug") << "  processing NonlinearExtension::check : "
                          << std::endl;
    Trace("nl-ext-debug") << "     " << false_asserts.size()
                          << " false assertions" << std::endl;
    Trace("nl-ext-debug") << "     " << xts.size()
                          << " extended terms: " << std::endl;
    Trace("nl-ext-debug") << "       ";
    for (unsigned j = 0; j < xts.size(); j++)
    {
      Trace("nl-ext-debug") << xts[j] << " ";
    }
    Trace("nl-ext-debug") << std::endl;
  }

  // compute whether shared terms have correct values
  unsigned num_shared_wrong_value = 0;
  std::vector<Node> shared_term_value_splits;
  // must ensure that shared terms are equal to their concrete value
  Trace("nl-ext-mv") << "Shared terms : " << std::endl;
  for (context::CDList<TNode>::const_iterator its =
           d_containing.shared_terms_begin();
       its != d_containing.shared_terms_end();
       ++its)
  {
    TNode shared_term = *its;
    // compute its value in the model, and its evaluation in the model
    Node stv0 = d_model.computeConcreteModelValue(shared_term);
    Node stv1 = d_model.computeAbstractModelValue(shared_term);
    d_model.printModelValue("nl-ext-mv", shared_term);
    if (stv0 != stv1)
    {
      num_shared_wrong_value++;
      Trace("nl-ext-mv") << "Bad shared term value : " << shared_term
                         << std::endl;
      if (shared_term != stv0)
      {
        // split on the value, this is non-terminating in general, TODO :
        // improve this
        Node eq = shared_term.eqNode(stv0);
        shared_term_value_splits.push_back(eq);
      }
      else
      {
        // this can happen for transcendental functions
        // the problem is that we cannot evaluate transcendental functions
        // (they don't have a rewriter that returns constants)
        // thus, the actual value in their model can be themselves, hence we
        // have no reference point to rule out the current model.  In this
        // case, we may set incomplete below.
      }
    }
  }
  Trace("nl-ext-debug") << "     " << num_shared_wrong_value
                        << " shared terms with wrong model value." << std::endl;
  bool needsRecheck;
  do
  {
    d_model.resetCheck();
    needsRecheck = false;
    // complete_status:
    //   1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown
    int complete_status = 1;
    // We require a check either if an assertion is false or a shared term has
    // a wrong value
    if (!false_asserts.empty() || num_shared_wrong_value > 0)
    {
      complete_status = num_shared_wrong_value > 0 ? -1 : 0;
      runStrategy(Theory::Effort::EFFORT_FULL, assertions, false_asserts, xts);
      if (d_im.hasSentLemma() || d_im.hasPendingLemma())
      {
        d_im.clearWaitingLemmas();
        return Result::Sat::UNSAT;
      }
    }
    Trace("nl-ext") << "Finished check with status : " << complete_status
                    << std::endl;

    // if we did not add a lemma during check and there is a chance for SAT
    if (complete_status == 0)
    {
      Trace("nl-ext")
          << "Check model based on bounds for irrational-valued functions..."
          << std::endl;
      // check the model based on simple solving of equalities and using
      // error bounds on the Taylor approximation of transcendental functions.
      if (checkModel(assertions))
      {
        complete_status = 1;
      }
      if (d_im.hasUsed())
      {
        d_im.clearWaitingLemmas();
        return Result::Sat::UNSAT;
      }
    }

    // if we have not concluded SAT
    if (complete_status != 1)
    {
      // flush the waiting lemmas
      if (d_im.hasWaitingLemma())
      {
        std::size_t count = d_im.numWaitingLemmas();
        d_im.flushWaitingLemmas();
        Trace("nl-ext") << "...added " << count << " waiting lemmas."
                        << std::endl;
        return Result::Sat::UNSAT;
      }
      // resort to splitting on shared terms with their model value
      // if we did not add any lemmas
      if (num_shared_wrong_value > 0)
      {
        complete_status = -1;
        if (!shared_term_value_splits.empty())
        {
          for (const Node& eq : shared_term_value_splits)
          {
            Node req = Rewriter::rewrite(eq);
            Node literal = d_containing.getValuation().ensureLiteral(req);
            d_containing.getOutputChannel().requirePhase(literal, true);
            Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
            Node split = literal.orNode(literal.negate());
            d_im.addPendingLemma(split,
                                 InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT,
                                 nullptr,
                                 true);
          }
          if (d_im.hasWaitingLemma())
          {
            d_im.flushWaitingLemmas();
            Trace("nl-ext") << "...added " << d_im.numPendingLemmas()
                            << " shared term value split lemmas." << std::endl;
            return Result::Sat::UNSAT;
          }
        }
        else
        {
          // this can happen if we are trying to do theory combination with
          // trancendental functions
          // since their model value cannot even be computed exactly
        }
      }

      // we are incomplete
      if (options::nlExt() == options::NlExtMode::FULL
          && options::nlExtIncPrecision() && d_model.usedApproximate())
      {
        d_trSlv.incrementTaylorDegree();
        needsRecheck = true;
        // increase precision for PI?
        // Difficult since Taylor series is very slow to converge
        Trace("nl-ext") << "...increment Taylor degree to "
                        << d_trSlv.getTaylorDegree() << std::endl;
      }
      else
      {
        Trace("nl-ext") << "...failed to send lemma in "
                           "NonLinearExtension, set incomplete"
                        << std::endl;
        d_containing.getOutputChannel().setIncomplete(IncompleteId::ARITH_NL);
        return Result::Sat::SAT_UNKNOWN;
      }
    }
    d_im.clearWaitingLemmas();
  } while (needsRecheck);

  // did not add lemmas
  return Result::Sat::SAT;
}

void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel,
                                        const std::set<Node>& termSet)
{
  if (!needsCheckLastEffort())
  {
    // no non-linear constraints, we are done
    return;
  }
  Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl;
  d_model.reset(d_containing.getValuation().getModel(), arithModel);
  // run a last call effort check
  Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
  Result::Sat res = modelBasedRefinement(termSet);
  if (res == Result::Sat::SAT)
  {
    Trace("nl-ext") << "interceptModel: do model repair" << std::endl;
    d_approximations.clear();
    d_witnesses.clear();
    // modify the model values
    d_model.getModelValueRepair(arithModel, d_approximations, d_witnesses);
  }
}

void NonlinearExtension::presolve()
{
  Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl;
}

void NonlinearExtension::runStrategy(Theory::Effort effort,
                                     const std::vector<Node>& assertions,
                                     const std::vector<Node>& false_asserts,
                                     const std::vector<Node>& xts)
{
  ++(d_stats.d_checkRuns);

  if (Trace.isOn("nl-strategy"))
  {
    for (const auto& a : assertions)
    {
      Trace("nl-strategy") << "Input assertion: " << a << std::endl;
    }
  }
  if (!d_strategy.isStrategyInit())
  {
    d_strategy.initializeStrategy();
  }

  auto steps = d_strategy.getStrategy();
  bool stop = false;
  while (!stop && steps.hasNext())
  {
    InferStep step = steps.next();
    Trace("nl-strategy") << "Step " << step << std::endl;
    switch (step)
    {
      case InferStep::BREAK: stop = d_im.hasPendingLemma(); break;
      case InferStep::FLUSH_WAITING_LEMMAS: d_im.flushWaitingLemmas(); break;
      case InferStep::CAD_FULL: d_cadSlv.checkFull(); break;
      case InferStep::CAD_INIT: d_cadSlv.initLastCall(assertions); break;
      case InferStep::NL_FACTORING:
        d_factoringSlv.check(assertions, false_asserts);
        break;
      case InferStep::IAND_INIT:
        d_iandSlv.initLastCall(assertions, false_asserts, xts);
        break;
      case InferStep::IAND_FULL: d_iandSlv.checkFullRefine(); break;
      case InferStep::IAND_INITIAL: d_iandSlv.checkInitialRefine(); break;
      case InferStep::POW2_INIT:
        d_pow2Slv.initLastCall(assertions, false_asserts, xts);
        break;
      case InferStep::POW2_FULL: d_pow2Slv.checkFullRefine(); break;
      case InferStep::POW2_INITIAL: d_pow2Slv.checkInitialRefine(); break;
      case InferStep::ICP:
        d_icpSlv.reset(assertions);
        d_icpSlv.check();
        break;
      case InferStep::NL_INIT:
        d_extState.init(xts);
        d_monomialBoundsSlv.init();
        d_monomialSlv.init(xts);
        break;
      case InferStep::NL_MONOMIAL_INFER_BOUNDS:
        d_monomialBoundsSlv.checkBounds(assertions, false_asserts);
        break;
      case InferStep::NL_MONOMIAL_MAGNITUDE0:
        d_monomialSlv.checkMagnitude(0);
        break;
      case InferStep::NL_MONOMIAL_MAGNITUDE1:
        d_monomialSlv.checkMagnitude(1);
        break;
      case InferStep::NL_MONOMIAL_MAGNITUDE2:
        d_monomialSlv.checkMagnitude(2);
        break;
      case InferStep::NL_MONOMIAL_SIGN: d_monomialSlv.checkSign(); break;
      case InferStep::NL_RESOLUTION_BOUNDS:
        d_monomialBoundsSlv.checkResBounds();
        break;
      case InferStep::NL_SPLIT_ZERO: d_splitZeroSlv.check(); break;
      case InferStep::NL_TANGENT_PLANES: d_tangentPlaneSlv.check(false); break;
      case InferStep::NL_TANGENT_PLANES_WAITING:
        d_tangentPlaneSlv.check(true);
        break;
      case InferStep::TRANS_INIT:
        d_trSlv.initLastCall(xts);
        break;
      case InferStep::TRANS_INITIAL:
        d_trSlv.checkTranscendentalInitialRefine();
        break;
      case InferStep::TRANS_MONOTONIC:
        d_trSlv.checkTranscendentalMonotonic();
        break;
      case InferStep::TRANS_TANGENT_PLANES:
        d_trSlv.checkTranscendentalTangentPlanes();
        break;
    }
  }

  Trace("nl-ext") << "finished strategy" << std::endl;
  Trace("nl-ext") << "  ...finished with " << d_im.numWaitingLemmas()
                  << " waiting lemmas." << std::endl;
  Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas()
                  << " pending lemmas." << std::endl;
}

}  // namespace nl
}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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