Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/nonlinear_extension.cpp	Lines:	285	319	89.3 %
Date:	2021-05-21	Branches:	487	966	50.4 %


/******************************************************************************
 * 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"

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