Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/ext/monomial_bounds_check.cpp	Lines:	171	294	58.2 %
Date:	2021-09-18	Branches:	366	1190	30.8 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Check for monomial bound inference lemmas.
 */

#include "theory/arith/nl/ext/monomial_bounds_check.h"

#include "expr/node.h"
#include "options/arith_options.h"
#include "proof/proof.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/ext/ext_state.h"
#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"

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

namespace {
void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs)
{
  Node t = ArithMSum::mkCoeffTerm(coeff, x);
  Trace(c) << t << " " << type << " " << rhs;
}

bool hasNewMonomials(Node n, const std::vector<Node>& existing)
{
  std::set<Node> visited;

  std::vector<Node> worklist;
  worklist.push_back(n);
  while (!worklist.empty())
  {
    Node current = worklist.back();
    worklist.pop_back();
    if (visited.find(current) == visited.end())
    {
      visited.insert(current);
      if (current.getKind() == Kind::NONLINEAR_MULT)
      {
        if (std::find(existing.begin(), existing.end(), current)
            == existing.end())
        {
          return true;
        }
      }
      else
      {
        worklist.insert(worklist.end(), current.begin(), current.end());
      }
    }
  }
  return false;
}
}  // namespace

MonomialBoundsCheck::MonomialBoundsCheck(ExtState* data)
    : d_data(data), d_cdb(d_data->d_mdb)
{
}

void MonomialBoundsCheck::init()
{
  d_ci.clear();
  d_ci_exp.clear();
  d_ci_max.clear();
}

void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
                                      const std::vector<Node>& false_asserts)
{
  // sort monomials by degree
  Trace("nl-ext-proc") << "Sort monomials by degree..." << std::endl;
  d_data->d_mdb.sortByDegree(d_data->d_ms);
  // all monomials
  d_data->d_mterms.insert(d_data->d_mterms.end(),
                          d_data->d_ms_vars.begin(),
                          d_data->d_ms_vars.end());
  d_data->d_mterms.insert(
      d_data->d_mterms.end(), d_data->d_ms.begin(), d_data->d_ms.end());

  const std::map<Node, std::map<Node, ConstraintInfo> >& cim =
      d_cdb.getConstraints();

  NodeManager* nm = NodeManager::currentNM();
  // register constraints
  Trace("nl-ext-debug") << "Register bound constraints..." << std::endl;
  for (const Node& lit : asserts)
  {
    bool polarity = lit.getKind() != Kind::NOT;
    Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
    d_cdb.registerConstraint(atom);
    bool is_false_lit =
        std::find(false_asserts.begin(), false_asserts.end(), lit)
        != false_asserts.end();
    // add information about bounds to variables
    std::map<Node, std::map<Node, ConstraintInfo> >::const_iterator itc =
        cim.find(atom);
    if (itc == cim.end())
    {
      continue;
    }
    for (const std::pair<const Node, ConstraintInfo>& itcc : itc->second)
    {
      Node x = itcc.first;
      Node coeff = itcc.second.d_coeff;
      Node rhs = itcc.second.d_rhs;
      Kind type = itcc.second.d_type;
      Node exp = lit;
      if (!polarity)
      {
        // reverse
        if (type == Kind::EQUAL)
        {
          // we will take the strict inequality in the direction of the
          // model
          Node lhs = ArithMSum::mkCoeffTerm(coeff, x);
          Node query = nm->mkNode(Kind::GT, lhs, rhs);
          Node query_mv = d_data->d_model.computeAbstractModelValue(query);
          if (query_mv == d_data->d_true)
          {
            exp = query;
            type = Kind::GT;
          }
          else
          {
            Assert(query_mv == d_data->d_false);
            exp = nm->mkNode(Kind::LT, lhs, rhs);
            type = Kind::LT;
          }
        }
        else
        {
          type = negateKind(type);
        }
      }
      // add to status if maximal degree
      d_ci_max[x][coeff][rhs] = d_cdb.isMaximal(atom, x);
      if (Trace.isOn("nl-ext-bound-debug2"))
      {
        Node t = ArithMSum::mkCoeffTerm(coeff, x);
        Trace("nl-ext-bound-debug2") << "Add Bound: " << t << " " << type << " "
                                     << rhs << " by " << exp << std::endl;
      }
      bool updated = true;
      std::map<Node, Kind>::iterator its = d_ci[x][coeff].find(rhs);
      if (its == d_ci[x][coeff].end())
      {
        d_ci[x][coeff][rhs] = type;
        d_ci_exp[x][coeff][rhs] = exp;
      }
      else if (type != its->second)
      {
        Trace("nl-ext-bound-debug2")
            << "Joining kinds : " << type << " " << its->second << std::endl;
        Kind jk = joinKinds(type, its->second);
        if (jk == Kind::UNDEFINED_KIND)
        {
          updated = false;
        }
        else if (jk != its->second)
        {
          if (jk == type)
          {
            d_ci[x][coeff][rhs] = type;
            d_ci_exp[x][coeff][rhs] = exp;
          }
          else
          {
            d_ci[x][coeff][rhs] = jk;
            d_ci_exp[x][coeff][rhs] =
                nm->mkNode(Kind::AND, d_ci_exp[x][coeff][rhs], exp);
          }
        }
        else
        {
          updated = false;
        }
      }
      if (Trace.isOn("nl-ext-bound"))
      {
        if (updated)
        {
          Trace("nl-ext-bound") << "Bound: ";
          debugPrintBound("nl-ext-bound", coeff, x, d_ci[x][coeff][rhs], rhs);
          Trace("nl-ext-bound") << " by " << d_ci_exp[x][coeff][rhs];
          if (d_ci_max[x][coeff][rhs])
          {
            Trace("nl-ext-bound") << ", is max degree";
          }
          Trace("nl-ext-bound") << std::endl;
        }
      }
      // compute if bound is not satisfied, and store what is required
      // for a possible refinement
      if (d_data->d_env.getOptions().arith.nlExtTangentPlanes)
      {
        if (is_false_lit)
        {
          d_data->d_tplane_refine.insert(x);
        }
      }
    }
  }
  // reflexive constraints
  Node null_coeff;
  for (unsigned j = 0; j < d_data->d_mterms.size(); j++)
  {
    Node n = d_data->d_mterms[j];
    d_ci[n][null_coeff][n] = Kind::EQUAL;
    d_ci_exp[n][null_coeff][n] = d_data->d_true;
    d_ci_max[n][null_coeff][n] = false;
  }

  Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl;
  const std::map<Node, std::vector<Node> >& cpMap =
      d_data->d_mdb.getContainsParentMap();
  for (unsigned k = 0; k < d_data->d_mterms.size(); k++)
  {
    Node x = d_data->d_mterms[k];
    Trace("nl-ext-bound-debug")
        << "Process bounds for " << x << " : " << std::endl;
    std::map<Node, std::vector<Node> >::const_iterator itm = cpMap.find(x);
    if (itm == cpMap.end())
    {
      Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl;
      continue;
    }
    Trace("nl-ext-bound-debug")
        << "...has " << itm->second.size() << " parent monomials." << std::endl;
    // check derived bounds
    std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc =
        d_ci.find(x);
    if (itc == d_ci.end())
    {
      continue;
    }
    for (std::map<Node, std::map<Node, Kind> >::iterator itcc =
             itc->second.begin();
         itcc != itc->second.end();
         ++itcc)
    {
      Node coeff = itcc->first;
      Node t = ArithMSum::mkCoeffTerm(coeff, x);
      for (std::map<Node, Kind>::iterator itcr = itcc->second.begin();
           itcr != itcc->second.end();
           ++itcr)
      {
        Node rhs = itcr->first;
        // only consider this bound if maximal degree
        if (!d_ci_max[x][coeff][rhs])
        {
          continue;
        }
        Kind type = itcr->second;
        for (unsigned j = 0; j < itm->second.size(); j++)
        {
          Node y = itm->second[j];
          Node mult = d_data->d_mdb.getContainsDiff(x, y);
          // x <k> t => m*x <k'> t  where y = m*x
          // get the sign of mult
          Node mmv = d_data->d_model.computeConcreteModelValue(mult);
          Trace("nl-ext-bound-debug2")
              << "Model value of " << mult << " is " << mmv << std::endl;
          if (!mmv.isConst())
          {
            Trace("nl-ext-bound-debug")
                << "     ...coefficient " << mult
                << " is non-constant (probably transcendental)." << std::endl;
            continue;
          }
          int mmv_sign = mmv.getConst<Rational>().sgn();
          Trace("nl-ext-bound-debug2")
              << "  sign of " << mmv << " is " << mmv_sign << std::endl;
          if (mmv_sign == 0)
          {
            Trace("nl-ext-bound-debug")
                << "     ...coefficient " << mult << " is zero." << std::endl;
            continue;
          }
          Trace("nl-ext-bound-debug")
              << "  from " << x << " * " << mult << " = " << y << " and " << t
              << " " << type << " " << rhs << ", infer : " << std::endl;
          Kind infer_type = mmv_sign == -1 ? reverseRelationKind(type) : type;
          Node infer_lhs = nm->mkNode(Kind::MULT, mult, t);
          Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhs);
          Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs);
          Trace("nl-ext-bound-debug") << "     " << infer << std::endl;
          Node infer_mv = d_data->d_model.computeAbstractModelValue(Rewriter::rewrite(infer));
          Trace("nl-ext-bound-debug")
              << "       ...infer model value is " << infer_mv << std::endl;
          if (infer_mv == d_data->d_false)
          {
            Node exp = nm->mkNode(
                Kind::AND,
                nm->mkNode(
                    mmv_sign == 1 ? Kind::GT : Kind::LT, mult, d_data->d_zero),
                d_ci_exp[x][coeff][rhs]);
            Node iblem = nm->mkNode(Kind::IMPLIES, exp, infer);
            Node iblem_rw = Rewriter::rewrite(iblem);
            bool introNewTerms = hasNewMonomials(iblem_rw, d_data->d_ms);
            Trace("nl-ext-bound-lemma")
                << "*** Bound inference lemma : " << iblem_rw
                << " (pre-rewrite : " << iblem << ")" << std::endl;
            CDProof* proof = nullptr;
            Node orig = d_ci_exp[x][coeff][rhs];
            if (d_data->isProofEnabled())
            {
              proof = d_data->getProof();
              // this is iblem, but uses (type t rhs) instead of the original
              // variant (which is identical under rewriting)
              // we first infer the "clean" version of the lemma and then
              // use MACRO_SR_PRED_TRANSFORM to rewrite
              Node tmplem = nm->mkNode(
                  Kind::IMPLIES,
                  nm->mkNode(Kind::AND,
                             nm->mkNode(mmv_sign == 1 ? Kind::GT : Kind::LT,
                                        mult,
                                        d_data->d_zero),
                             nm->mkNode(type, t, rhs)),
                  infer);
              proof->addStep(tmplem,
                             mmv_sign == 1 ? PfRule::ARITH_MULT_POS
                                           : PfRule::ARITH_MULT_NEG,
                             {},
                             {mult, nm->mkNode(type, t, rhs)});
              proof->addStep(
                  iblem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {iblem});
            }
            d_data->d_im.addPendingLemma(iblem,
                                         InferenceId::ARITH_NL_INFER_BOUNDS_NT,
                                         proof,
                                         introNewTerms);
          }
        }
      }
    }
  }
}

void MonomialBoundsCheck::checkResBounds()
{
  NodeManager* nm = NodeManager::currentNM();
  Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..."
                  << std::endl;
  size_t nmterms = d_data->d_mterms.size();
  for (unsigned j = 0; j < nmterms; j++)
  {
    Node a = d_data->d_mterms[j];
    std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca =
        d_ci.find(a);
    if (itca == d_ci.end())
    {
      continue;
    }
    for (unsigned k = (j + 1); k < nmterms; k++)
    {
      Node b = d_data->d_mterms[k];
      std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itcb =
          d_ci.find(b);
      if (itcb == d_ci.end())
      {
        continue;
      }
      Trace("nl-ext-rbound-debug") << "resolution inferences : compare " << a
                                   << " and " << b << std::endl;
      // if they have common factors
      std::map<Node, Node>::iterator ita = d_data->d_mono_diff[a].find(b);
      if (ita == d_data->d_mono_diff[a].end())
      {
        continue;
      }
      Trace("nl-ext-rbound") << "Get resolution inferences for [a] " << a
                             << " vs [b] " << b << std::endl;
      std::map<Node, Node>::iterator itb = d_data->d_mono_diff[b].find(a);
      Assert(itb != d_data->d_mono_diff[b].end());
      Node mv_a = d_data->d_model.computeAbstractModelValue(ita->second);
      Assert(mv_a.isConst());
      int mv_a_sgn = mv_a.getConst<Rational>().sgn();
      if (mv_a_sgn == 0)
      {
        // we don't compare monomials whose current model value is zero
        continue;
      }
      Node mv_b = d_data->d_model.computeAbstractModelValue(itb->second);
      Assert(mv_b.isConst());
      int mv_b_sgn = mv_b.getConst<Rational>().sgn();
      if (mv_b_sgn == 0)
      {
        // we don't compare monomials whose current model value is zero
        continue;
      }
      Trace("nl-ext-rbound") << "  [a] factor is " << ita->second
                             << ", sign in model = " << mv_a_sgn << std::endl;
      Trace("nl-ext-rbound") << "  [b] factor is " << itb->second
                             << ", sign in model = " << mv_b_sgn << std::endl;

      std::vector<Node> exp;
      // bounds of a
      for (std::map<Node, std::map<Node, Kind> >::iterator itcac =
               itca->second.begin();
           itcac != itca->second.end();
           ++itcac)
      {
        Node coeff_a = itcac->first;
        for (std::map<Node, Kind>::iterator itcar = itcac->second.begin();
             itcar != itcac->second.end();
             ++itcar)
        {
          Node rhs_a = itcar->first;
          Node rhs_a_res_base = nm->mkNode(Kind::MULT, itb->second, rhs_a);
          rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
          if (hasNewMonomials(rhs_a_res_base, d_data->d_ms))
          {
            continue;
          }
          Kind type_a = itcar->second;
          exp.push_back(d_ci_exp[a][coeff_a][rhs_a]);

          // bounds of b
          for (std::map<Node, std::map<Node, Kind> >::iterator itcbc =
                   itcb->second.begin();
               itcbc != itcb->second.end();
               ++itcbc)
          {
            Node coeff_b = itcbc->first;
            Node rhs_a_res = ArithMSum::mkCoeffTerm(coeff_b, rhs_a_res_base);
            for (std::map<Node, Kind>::iterator itcbr = itcbc->second.begin();
                 itcbr != itcbc->second.end();
                 ++itcbr)
            {
              Node rhs_b = itcbr->first;
              Node rhs_b_res = nm->mkNode(Kind::MULT, ita->second, rhs_b);
              rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res);
              rhs_b_res = Rewriter::rewrite(rhs_b_res);
              if (hasNewMonomials(rhs_b_res, d_data->d_ms))
              {
                continue;
              }
              Kind type_b = itcbr->second;
              exp.push_back(d_ci_exp[b][coeff_b][rhs_b]);
              if (Trace.isOn("nl-ext-rbound"))
              {
                Trace("nl-ext-rbound") << "* try bounds : ";
                debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, rhs_a);
                Trace("nl-ext-rbound") << std::endl;
                Trace("nl-ext-rbound") << "               ";
                debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, rhs_b);
                Trace("nl-ext-rbound") << std::endl;
              }
              Kind types[2];
              for (unsigned r = 0; r < 2; r++)
              {
                Node pivot_factor = r == 0 ? itb->second : ita->second;
                int pivot_factor_sign = r == 0 ? mv_b_sgn : mv_a_sgn;
                types[r] = r == 0 ? type_a : type_b;
                if (pivot_factor_sign == (r == 0 ? 1 : -1))
                {
                  types[r] = reverseRelationKind(types[r]);
                }
                if (pivot_factor_sign == 1)
                {
                  exp.push_back(
                      nm->mkNode(Kind::GT, pivot_factor, d_data->d_zero));
                }
                else
                {
                  exp.push_back(
                      nm->mkNode(Kind::LT, pivot_factor, d_data->d_zero));
                }
              }
              Kind jk = transKinds(types[0], types[1]);
              Trace("nl-ext-rbound-debug")
                  << "trans kind : " << types[0] << " + " << types[1] << " = "
                  << jk << std::endl;
              if (jk != Kind::UNDEFINED_KIND)
              {
                Node conc = nm->mkNode(jk, rhs_a_res, rhs_b_res);
                Node conc_mv = d_data->d_model.computeAbstractModelValue(conc);
                if (conc_mv == d_data->d_false)
                {
                  Node rblem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc);
                  Trace("nl-ext-rbound-lemma-debug")
                      << "Resolution bound lemma "
                         "(pre-rewrite) "
                         ": "
                      << rblem << std::endl;
                  rblem = Rewriter::rewrite(rblem);
                  Trace("nl-ext-rbound-lemma")
                      << "Resolution bound lemma : " << rblem << std::endl;
                  d_data->d_im.addPendingLemma(
                      rblem, InferenceId::ARITH_NL_RES_INFER_BOUNDS);
                }
              }
              exp.pop_back();
              exp.pop_back();
              exp.pop_back();
            }
          }
          exp.pop_back();
        }
      }
    }
  }
}

}  // 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		* Check for monomial bound inference lemmas.
14		*/
15
16		#include "theory/arith/nl/ext/monomial_bounds_check.h"
17
18		#include "expr/node.h"
19		#include "options/arith_options.h"
20		#include "proof/proof.h"
21		#include "theory/arith/arith_msum.h"
22		#include "theory/arith/arith_utilities.h"
23		#include "theory/arith/inference_manager.h"
24		#include "theory/arith/nl/ext/ext_state.h"
25		#include "theory/arith/nl/nl_model.h"
26		#include "theory/rewriter.h"
27
28		namespace cvc5 {
29		namespace theory {
30		namespace arith {
31		namespace nl {
32
33		namespace {
34		void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs)
35		{
36		Node t = ArithMSum::mkCoeffTerm(coeff, x);
37		Trace(c) << t << " " << type << " " << rhs;
38		}
39
40	4354	bool hasNewMonomials(Node n, const std::vector<Node>& existing)
41		{
42	8708	std::set<Node> visited;
43
44	8708	std::vector<Node> worklist;
45	4354	worklist.push_back(n);
46	82932	while (!worklist.empty())
47		{
48	81898	Node current = worklist.back();
49	42609	worklist.pop_back();
50	42609	if (visited.find(current) == visited.end())
51		{
52	39494	visited.insert(current);
53	39494	if (current.getKind() == Kind::NONLINEAR_MULT)
54		{
55	19377	if (std::find(existing.begin(), existing.end(), current)
56	19377	== existing.end())
57		{
58	3320	return true;
59		}
60		}
61		else
62		{
63	33035	worklist.insert(worklist.end(), current.begin(), current.end());
64		}
65		}
66		}
67	1034	return false;
68		}
69		} // namespace
70
71	5203	MonomialBoundsCheck::MonomialBoundsCheck(ExtState* data)
72	5203	: d_data(data), d_cdb(d_data->d_mdb)
73		{
74	5203	}
75
76	3990	void MonomialBoundsCheck::init()
77		{
78	3990	d_ci.clear();
79	3990	d_ci_exp.clear();
80	3990	d_ci_max.clear();
81	3990	}
82
83	743	void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
84		const std::vector<Node>& false_asserts)
85		{
86		// sort monomials by degree
87	743	Trace("nl-ext-proc") << "Sort monomials by degree..." << std::endl;
88	743	d_data->d_mdb.sortByDegree(d_data->d_ms);
89		// all monomials
90	2972	d_data->d_mterms.insert(d_data->d_mterms.end(),
91	743	d_data->d_ms_vars.begin(),
92	2972	d_data->d_ms_vars.end());
93	1486	d_data->d_mterms.insert(
94	1486	d_data->d_mterms.end(), d_data->d_ms.begin(), d_data->d_ms.end());
95
96		const std::map<Node, std::map<Node, ConstraintInfo> >& cim =
97	743	d_cdb.getConstraints();
98
99	743	NodeManager* nm = NodeManager::currentNM();
100		// register constraints
101	743	Trace("nl-ext-debug") << "Register bound constraints..." << std::endl;
102	61996	for (const Node& lit : asserts)
103		{
104	61253	bool polarity = lit.getKind() != Kind::NOT;
105	122506	Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
106	61253	d_cdb.registerConstraint(atom);
107		bool is_false_lit =
108	122506	std::find(false_asserts.begin(), false_asserts.end(), lit)
109	183759	!= false_asserts.end();
110		// add information about bounds to variables
111		std::map<Node, std::map<Node, ConstraintInfo> >::const_iterator itc =
112	61253	cim.find(atom);
113	61253	if (itc == cim.end())
114		{
115		continue;
116		}
117	168795	for (const std::pair<const Node, ConstraintInfo>& itcc : itc->second)
118		{
119	215084	Node x = itcc.first;
120	215084	Node coeff = itcc.second.d_coeff;
121	215084	Node rhs = itcc.second.d_rhs;
122	107542	Kind type = itcc.second.d_type;
123	215084	Node exp = lit;
124	107542	if (!polarity)
125		{
126		// reverse
127	60719	if (type == Kind::EQUAL)
128		{
129		// we will take the strict inequality in the direction of the
130		// model
131	48226	Node lhs = ArithMSum::mkCoeffTerm(coeff, x);
132	48226	Node query = nm->mkNode(Kind::GT, lhs, rhs);
133	48226	Node query_mv = d_data->d_model.computeAbstractModelValue(query);
134	24113	if (query_mv == d_data->d_true)
135		{
136	15119	exp = query;
137	15119	type = Kind::GT;
138		}
139		else
140		{
141	8994	Assert(query_mv == d_data->d_false);
142	8994	exp = nm->mkNode(Kind::LT, lhs, rhs);
143	8994	type = Kind::LT;
144		}
145		}
146		else
147		{
148	36606	type = negateKind(type);
149		}
150		}
151		// add to status if maximal degree
152	107542	d_ci_max[x][coeff][rhs] = d_cdb.isMaximal(atom, x);
153	107542	if (Trace.isOn("nl-ext-bound-debug2"))
154		{
155		Node t = ArithMSum::mkCoeffTerm(coeff, x);
156		Trace("nl-ext-bound-debug2") << "Add Bound: " << t << " " << type << " "
157		<< rhs << " by " << exp << std::endl;
158		}
159	107542	bool updated = true;
160	107542	std::map<Node, Kind>::iterator its = d_ci[x][coeff].find(rhs);
161	107542	if (its == d_ci[x][coeff].end())
162		{
163	93275	d_ci[x][coeff][rhs] = type;
164	93275	d_ci_exp[x][coeff][rhs] = exp;
165		}
166	14267	else if (type != its->second)
167		{
168	10594	Trace("nl-ext-bound-debug2")
169	5297	<< "Joining kinds : " << type << " " << its->second << std::endl;
170	5297	Kind jk = joinKinds(type, its->second);
171	5297	if (jk == Kind::UNDEFINED_KIND)
172		{
173		updated = false;
174		}
175	5297	else if (jk != its->second)
176		{
177	2896	if (jk == type)
178		{
179	2874	d_ci[x][coeff][rhs] = type;
180	2874	d_ci_exp[x][coeff][rhs] = exp;
181		}
182		else
183		{
184	22	d_ci[x][coeff][rhs] = jk;
185	22	d_ci_exp[x][coeff][rhs] =
186	44	nm->mkNode(Kind::AND, d_ci_exp[x][coeff][rhs], exp);
187		}
188		}
189		else
190		{
191	2401	updated = false;
192		}
193		}
194	107542	if (Trace.isOn("nl-ext-bound"))
195		{
196		if (updated)
197		{
198		Trace("nl-ext-bound") << "Bound: ";
199		debugPrintBound("nl-ext-bound", coeff, x, d_ci[x][coeff][rhs], rhs);
200		Trace("nl-ext-bound") << " by " << d_ci_exp[x][coeff][rhs];
201		if (d_ci_max[x][coeff][rhs])
202		{
203		Trace("nl-ext-bound") << ", is max degree";
204		}
205		Trace("nl-ext-bound") << std::endl;
206		}
207		}
208		// compute if bound is not satisfied, and store what is required
209		// for a possible refinement
210	107542	if (d_data->d_env.getOptions().arith.nlExtTangentPlanes)
211		{
212	7433	if (is_false_lit)
213		{
214	1652	d_data->d_tplane_refine.insert(x);
215		}
216		}
217		}
218		}
219		// reflexive constraints
220	1486	Node null_coeff;
221	6011	for (unsigned j = 0; j < d_data->d_mterms.size(); j++)
222		{
223	10536	Node n = d_data->d_mterms[j];
224	5268	d_ci[n][null_coeff][n] = Kind::EQUAL;
225	5268	d_ci_exp[n][null_coeff][n] = d_data->d_true;
226	5268	d_ci_max[n][null_coeff][n] = false;
227		}
228
229	743	Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl;
230		const std::map<Node, std::vector<Node> >& cpMap =
231	743	d_data->d_mdb.getContainsParentMap();
232	6011	for (unsigned k = 0; k < d_data->d_mterms.size(); k++)
233		{
234	7528	Node x = d_data->d_mterms[k];
235	10536	Trace("nl-ext-bound-debug")
236	5268	<< "Process bounds for " << x << " : " << std::endl;
237	5268	std::map<Node, std::vector<Node> >::const_iterator itm = cpMap.find(x);
238	8276	if (itm == cpMap.end())
239		{
240	3008	Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl;
241	3008	continue;
242		}
243	4520	Trace("nl-ext-bound-debug")
244	2260	<< "...has " << itm->second.size() << " parent monomials." << std::endl;
245		// check derived bounds
246		std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc =
247	2260	d_ci.find(x);
248	2260	if (itc == d_ci.end())
249		{
250		continue;
251		}
252	4115	for (std::map<Node, std::map<Node, Kind> >::iterator itcc =
253	2260	itc->second.begin();
254	6375	itcc != itc->second.end();
255		++itcc)
256		{
257	8230	Node coeff = itcc->first;
258	8230	Node t = ArithMSum::mkCoeffTerm(coeff, x);
259	41149	for (std::map<Node, Kind>::iterator itcr = itcc->second.begin();
260	41149	itcr != itcc->second.end();
261		++itcr)
262		{
263	56598	Node rhs = itcr->first;
264		// only consider this bound if maximal degree
265	37034	if (!d_ci_max[x][coeff][rhs])
266		{
267	17470	continue;
268		}
269	19564	Kind type = itcr->second;
270	90598	for (unsigned j = 0; j < itm->second.size(); j++)
271		{
272	133869	Node y = itm->second[j];
273	133869	Node mult = d_data->d_mdb.getContainsDiff(x, y);
274		// x <k> t => mx <k'> t where y = mx
275		// get the sign of mult
276	133869	Node mmv = d_data->d_model.computeConcreteModelValue(mult);
277	142068	Trace("nl-ext-bound-debug2")
278	71034	<< "Model value of " << mult << " is " << mmv << std::endl;
279	71676	if (!mmv.isConst())
280		{
281	1284	Trace("nl-ext-bound-debug")
282	642	<< " ...coefficient " << mult
283	642	<< " is non-constant (probably transcendental)." << std::endl;
284	642	continue;
285		}
286	70392	int mmv_sign = mmv.getConst<Rational>().sgn();
287	140784	Trace("nl-ext-bound-debug2")
288	70392	<< " sign of " << mmv << " is " << mmv_sign << std::endl;
289	77949	if (mmv_sign == 0)
290		{
291	15114	Trace("nl-ext-bound-debug")
292	7557	<< " ...coefficient " << mult << " is zero." << std::endl;
293	7557	continue;
294		}
295	125670	Trace("nl-ext-bound-debug")
296	62835	<< " from " << x << " * " << mult << " = " << y << " and " << t
297	62835	<< " " << type << " " << rhs << ", infer : " << std::endl;
298	62835	Kind infer_type = mmv_sign == -1 ? reverseRelationKind(type) : type;
299	125670	Node infer_lhs = nm->mkNode(Kind::MULT, mult, t);
300	125670	Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhs);
301	125670	Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs);
302	62835	Trace("nl-ext-bound-debug") << " " << infer << std::endl;
303	125670	Node infer_mv = d_data->d_model.computeAbstractModelValue(Rewriter::rewrite(infer));
304	125670	Trace("nl-ext-bound-debug")
305	62835	<< " ...infer model value is " << infer_mv << std::endl;
306	62835	if (infer_mv == d_data->d_false)
307		{
308		Node exp = nm->mkNode(
309		Kind::AND,
310	13062	nm->mkNode(
311	8708	mmv_sign == 1 ? Kind::GT : Kind::LT, mult, d_data->d_zero),
312	17416	d_ci_exp[x][coeff][rhs]);
313	8708	Node iblem = nm->mkNode(Kind::IMPLIES, exp, infer);
314	8708	Node iblem_rw = Rewriter::rewrite(iblem);
315	4354	bool introNewTerms = hasNewMonomials(iblem_rw, d_data->d_ms);
316	8708	Trace("nl-ext-bound-lemma")
317	4354	<< "*** Bound inference lemma : " << iblem_rw
318	4354	<< " (pre-rewrite : " << iblem << ")" << std::endl;
319	4354	CDProof* proof = nullptr;
320	8708	Node orig = d_ci_exp[x][coeff][rhs];
321	4354	if (d_data->isProofEnabled())
322		{
323	642	proof = d_data->getProof();
324		// this is iblem, but uses (type t rhs) instead of the original
325		// variant (which is identical under rewriting)
326		// we first infer the "clean" version of the lemma and then
327		// use MACRO_SR_PRED_TRANSFORM to rewrite
328		Node tmplem = nm->mkNode(
329		Kind::IMPLIES,
330	2568	nm->mkNode(Kind::AND,
331	1284	nm->mkNode(mmv_sign == 1 ? Kind::GT : Kind::LT,
332		mult,
333	642	d_data->d_zero),
334	1284	nm->mkNode(type, t, rhs)),
335	2568	infer);
336	2568	proof->addStep(tmplem,
337	642	mmv_sign == 1 ? PfRule::ARITH_MULT_POS
338		: PfRule::ARITH_MULT_NEG,
339		{},
340	1284	{mult, nm->mkNode(type, t, rhs)});
341	1926	proof->addStep(
342	1284	iblem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {iblem});
343		}
344	4354	d_data->d_im.addPendingLemma(iblem,
345		InferenceId::ARITH_NL_INFER_BOUNDS_NT,
346		proof,
347		introNewTerms);
348		}
349		}
350		}
351		}
352		}
353	743	}
354
355		void MonomialBoundsCheck::checkResBounds()
356		{
357		NodeManager* nm = NodeManager::currentNM();
358		Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..."
359		<< std::endl;
360		size_t nmterms = d_data->d_mterms.size();
361		for (unsigned j = 0; j < nmterms; j++)
362		{
363		Node a = d_data->d_mterms[j];
364		std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca =
365		d_ci.find(a);
366		if (itca == d_ci.end())
367		{
368		continue;
369		}
370		for (unsigned k = (j + 1); k < nmterms; k++)
371		{
372		Node b = d_data->d_mterms[k];
373		std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itcb =
374		d_ci.find(b);
375		if (itcb == d_ci.end())
376		{
377		continue;
378		}
379		Trace("nl-ext-rbound-debug") << "resolution inferences : compare " << a
380		<< " and " << b << std::endl;
381		// if they have common factors
382		std::map<Node, Node>::iterator ita = d_data->d_mono_diff[a].find(b);
383		if (ita == d_data->d_mono_diff[a].end())
384		{
385		continue;
386		}
387		Trace("nl-ext-rbound") << "Get resolution inferences for [a] " << a
388		<< " vs [b] " << b << std::endl;
389		std::map<Node, Node>::iterator itb = d_data->d_mono_diff[b].find(a);
390		Assert(itb != d_data->d_mono_diff[b].end());
391		Node mv_a = d_data->d_model.computeAbstractModelValue(ita->second);
392		Assert(mv_a.isConst());
393		int mv_a_sgn = mv_a.getConst<Rational>().sgn();
394		if (mv_a_sgn == 0)
395		{
396		// we don't compare monomials whose current model value is zero
397		continue;
398		}
399		Node mv_b = d_data->d_model.computeAbstractModelValue(itb->second);
400		Assert(mv_b.isConst());
401		int mv_b_sgn = mv_b.getConst<Rational>().sgn();
402		if (mv_b_sgn == 0)
403		{
404		// we don't compare monomials whose current model value is zero
405		continue;
406		}
407		Trace("nl-ext-rbound") << " [a] factor is " << ita->second
408		<< ", sign in model = " << mv_a_sgn << std::endl;
409		Trace("nl-ext-rbound") << " [b] factor is " << itb->second
410		<< ", sign in model = " << mv_b_sgn << std::endl;
411
412		std::vector<Node> exp;
413		// bounds of a
414		for (std::map<Node, std::map<Node, Kind> >::iterator itcac =
415		itca->second.begin();
416		itcac != itca->second.end();
417		++itcac)
418		{
419		Node coeff_a = itcac->first;
420		for (std::map<Node, Kind>::iterator itcar = itcac->second.begin();
421		itcar != itcac->second.end();
422		++itcar)
423		{
424		Node rhs_a = itcar->first;
425		Node rhs_a_res_base = nm->mkNode(Kind::MULT, itb->second, rhs_a);
426		rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
427		if (hasNewMonomials(rhs_a_res_base, d_data->d_ms))
428		{
429		continue;
430		}
431		Kind type_a = itcar->second;
432		exp.push_back(d_ci_exp[a][coeff_a][rhs_a]);
433
434		// bounds of b
435		for (std::map<Node, std::map<Node, Kind> >::iterator itcbc =
436		itcb->second.begin();
437		itcbc != itcb->second.end();
438		++itcbc)
439		{
440		Node coeff_b = itcbc->first;
441		Node rhs_a_res = ArithMSum::mkCoeffTerm(coeff_b, rhs_a_res_base);
442		for (std::map<Node, Kind>::iterator itcbr = itcbc->second.begin();
443		itcbr != itcbc->second.end();
444		++itcbr)
445		{
446		Node rhs_b = itcbr->first;
447		Node rhs_b_res = nm->mkNode(Kind::MULT, ita->second, rhs_b);
448		rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res);
449		rhs_b_res = Rewriter::rewrite(rhs_b_res);
450		if (hasNewMonomials(rhs_b_res, d_data->d_ms))
451		{
452		continue;
453		}
454		Kind type_b = itcbr->second;
455		exp.push_back(d_ci_exp[b][coeff_b][rhs_b]);
456		if (Trace.isOn("nl-ext-rbound"))
457		{
458		Trace("nl-ext-rbound") << "* try bounds : ";
459		debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, rhs_a);
460		Trace("nl-ext-rbound") << std::endl;
461		Trace("nl-ext-rbound") << " ";
462		debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, rhs_b);
463		Trace("nl-ext-rbound") << std::endl;
464		}
465		Kind types[2];
466		for (unsigned r = 0; r < 2; r++)
467		{
468		Node pivot_factor = r == 0 ? itb->second : ita->second;
469		int pivot_factor_sign = r == 0 ? mv_b_sgn : mv_a_sgn;
470		types[r] = r == 0 ? type_a : type_b;
471		if (pivot_factor_sign == (r == 0 ? 1 : -1))
472		{
473		types[r] = reverseRelationKind(types[r]);
474		}
475		if (pivot_factor_sign == 1)
476		{
477		exp.push_back(
478		nm->mkNode(Kind::GT, pivot_factor, d_data->d_zero));
479		}
480		else
481		{
482		exp.push_back(
483		nm->mkNode(Kind::LT, pivot_factor, d_data->d_zero));
484		}
485		}
486		Kind jk = transKinds(types[0], types[1]);
487		Trace("nl-ext-rbound-debug")
488		<< "trans kind : " << types[0] << " + " << types[1] << " = "
489		<< jk << std::endl;
490		if (jk != Kind::UNDEFINED_KIND)
491		{
492		Node conc = nm->mkNode(jk, rhs_a_res, rhs_b_res);
493		Node conc_mv = d_data->d_model.computeAbstractModelValue(conc);
494		if (conc_mv == d_data->d_false)
495		{
496		Node rblem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc);
497		Trace("nl-ext-rbound-lemma-debug")
498		<< "Resolution bound lemma "
499		"(pre-rewrite) "
500		": "
501		<< rblem << std::endl;
502		rblem = Rewriter::rewrite(rblem);
503		Trace("nl-ext-rbound-lemma")
504		<< "Resolution bound lemma : " << rblem << std::endl;
505		d_data->d_im.addPendingLemma(
506		rblem, InferenceId::ARITH_NL_RES_INFER_BOUNDS);
507		}
508		}
509		exp.pop_back();
510		exp.pop_back();
511		exp.pop_back();
512		}
513		}
514		exp.pop_back();
515		}
516		}
517		}
518		}
519		}
520
521		} // namespace nl
522		} // namespace arith
523		} // namespace theory
524	29574	} // namespace cvc5