Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/nonlinear_extension.cpp	Lines:	280	313	89.5 %
Date:	2021-11-07	Branches:	483	943	51.2 %


/******************************************************************************
 * 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 "options/smt_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(Env& env,
                                       TheoryArith& containing,
                                       ArithState& state)
    : EnvObj(env),
      d_containing(containing),
      d_astate(state),
      d_im(containing.getInferenceManager()),
      d_hasNlTerms(false),
      d_checkCounter(0),
      d_extTheoryCb(state.getEqualityEngine()),
      d_extTheory(env, d_extTheoryCb, d_im),
      d_model(),
      d_trSlv(d_env, d_im, d_model),
      d_extState(d_im, d_model, d_env),
      d_factoringSlv(d_env, &d_extState),
      d_monomialBoundsSlv(d_env, &d_extState),
      d_monomialSlv(d_env, &d_extState),
      d_splitZeroSlv(d_env, &d_extState),
      d_tangentPlaneSlv(d_env, &d_extState),
      d_cadSlv(d_env, d_im, d_model),
      d_icpSlv(d_env, d_im),
      d_iandSlv(env, d_im, state, d_model),
      d_pow2Slv(env, 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));

  if (d_env.isTheoryProofProducing())
  {
    ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
    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)
{
  const Valuation& v = d_containing.getValuation();
  for (const Node& a : assertions)
  {
    if (v.isRelevant(a))
    {
      keep.emplace_back(a);
    }
  }
  Trace("nl-ext-rlv") << "...relevant assertions: " << keep.size() << "/"
                      << assertions.size() << std::endl;
}

void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
{
  Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl;
  bool useRelevance = false;
  if (options().arith.nlRlvMode == options::NlRlvMode::INTERLEAVE)
  {
    useRelevance = (d_checkCounter % 2);
  }
  else if (options().arith.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 using the bound inference utility
    if (options().arith.nlRlvAssertBounds && 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::getUnsatisfiedAssertions(
    const std::vector<Node>& assertions)
{
  std::vector<Node> false_asserts;
  for (const auto& lit : assertions)
  {
    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]";
      false_asserts.push_back(lit);
    }
    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().arith.nlExt == options::NlExtMode::FULL)
  {
    // preprocess the assertions with the trancendental solver
    if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
    {
      return false;
    }
  }
  if (options().arith.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::checkFullEffort(std::map<Node, Node>& arithModel,
                                         const std::set<Node>& termSet)
{
  Trace("nl-ext") << "NonlinearExtension::checkFullEffort" << std::endl;

  d_hasNlTerms = true;
  if (options().arith.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_hasNlTerms = false;
      }
    }
    else
    {
      Trace("nl-ext") << "...sent lemmas." << std::endl;
    }
  }

  if (!hasNlTerms())
  {
    // 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,
                                options().smt.modelWitnessValue);
  }
}

void NonlinearExtension::finalizeModel(TheoryModel* tm)
{
  Trace("nl-ext") << "NonlinearExtension::finalizeModel" << std::endl;

  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 = getUnsatisfiedAssertions(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 = 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().arith.nlExt == options::NlExtMode::FULL
          && options().arith.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::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(options());
  }

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