Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/ext/tangent_plane_check.cpp	Lines:	72	73	98.6 %
Date:	2021-08-14	Branches:	189	350	54.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer, Andrew Reynolds, 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.
 * ****************************************************************************
 *
 * Implementation of tangent_plane check.
 */

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

#include "expr/node.h"
#include "proof/proof.h"
#include "theory/arith/arith_msum.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"
#include "util/rational.h"

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

TangentPlaneCheck::TangentPlaneCheck(ExtState* data) : d_data(data) {}

void TangentPlaneCheck::check(bool asWaitingLemmas)
{
  Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl;
  NodeManager* nm = NodeManager::currentNM();
  const std::map<Node, std::vector<Node> >& ccMap =
      d_data->d_mdb.getContainsChildrenMap();
  unsigned kstart = d_data->d_ms_vars.size();
  for (unsigned k = kstart; k < d_data->d_mterms.size(); k++)
  {
    Node t = d_data->d_mterms[k];
    // if this term requires a refinement
    if (d_data->d_tplane_refine.find(t) == d_data->d_tplane_refine.end())
    {
      continue;
    }
    Trace("nl-ext-tplanes")
        << "Look at monomial requiring refinement : " << t << std::endl;
    // get a decomposition
    std::map<Node, std::vector<Node> >::const_iterator it = ccMap.find(t);
    if (it == ccMap.end())
    {
      continue;
    }
    std::map<Node, std::map<Node, bool> > dproc;
    for (unsigned j = 0; j < it->second.size(); j++)
    {
      Node tc = it->second[j];
      if (tc != d_data->d_one)
      {
        Node tc_diff = d_data->d_mdb.getContainsDiffNl(tc, t);
        Assert(!tc_diff.isNull());
        Node a = tc < tc_diff ? tc : tc_diff;
        Node b = tc < tc_diff ? tc_diff : tc;
        if (dproc[a].find(b) == dproc[a].end())
        {
          dproc[a][b] = true;
          Trace("nl-ext-tplanes")
              << "  decomposable into : " << a << " * " << b << std::endl;
          Node a_v_c = d_data->d_model.computeAbstractModelValue(a);
          Node b_v_c = d_data->d_model.computeAbstractModelValue(b);
          // points we will add tangent planes for
          std::vector<Node> pts[2];
          pts[0].push_back(a_v_c);
          pts[1].push_back(b_v_c);
          // if previously refined
          bool prevRefine = d_tangent_val_bound[0][a].find(b)
                            != d_tangent_val_bound[0][a].end();
          // a_min, a_max, b_min, b_max
          for (unsigned p = 0; p < 4; p++)
          {
            Node curr_v = p <= 1 ? a_v_c : b_v_c;
            if (prevRefine)
            {
              Node pt_v = d_tangent_val_bound[p][a][b];
              Assert(!pt_v.isNull());
              if (curr_v != pt_v)
              {
                Node do_extend = nm->mkNode(
                    (p == 1 || p == 3) ? Kind::GT : Kind::LT, curr_v, pt_v);
                do_extend = Rewriter::rewrite(do_extend);
                if (do_extend == d_data->d_true)
                {
                  for (unsigned q = 0; q < 2; q++)
                  {
                    pts[p <= 1 ? 0 : 1].push_back(curr_v);
                    pts[p <= 1 ? 1 : 0].push_back(
                        d_tangent_val_bound[p <= 1 ? 2 + q : q][a][b]);
                  }
                }
              }
            }
            else
            {
              d_tangent_val_bound[p][a][b] = curr_v;
            }
          }

          for (unsigned p = 0; p < pts[0].size(); p++)
          {
            Node a_v = pts[0][p];
            Node b_v = pts[1][p];

            // tangent plane
            Node tplane = nm->mkNode(Kind::MINUS,
                                     nm->mkNode(Kind::PLUS,
                                                nm->mkNode(Kind::MULT, b_v, a),
                                                nm->mkNode(Kind::MULT, a_v, b)),
                                     nm->mkNode(Kind::MULT, a_v, b_v));
            // construct the following lemmas:
            // t <= tplane  <=>  ((a <= a_v ^ b >= b_v) v (a >= a_v ^ b <= b_v))
            // t >= tplane  <=>  ((a <= a_v ^ b <= b_v) v (a >= a_v ^ b >= b_v))

            for (unsigned d = 0; d < 2; d++)
            {
              Node b1 = nm->mkNode(d == 0 ? Kind::GEQ : Kind::LEQ, b, b_v);
              Node b2 = nm->mkNode(d == 0 ? Kind::LEQ : Kind::GEQ, b, b_v);
              Node tlem = nm->mkNode(
                  Kind::EQUAL,
                  nm->mkNode(d == 0 ? Kind::LEQ : Kind::GEQ, t, tplane),
                  nm->mkNode(
                      Kind::OR,
                      nm->mkNode(Kind::AND, nm->mkNode(Kind::LEQ, a, a_v), b1),
                      nm->mkNode(
                          Kind::AND, nm->mkNode(Kind::GEQ, a, a_v), b2)));
              Trace("nl-ext-tplanes")
                  << "Tangent plane lemma : " << tlem << std::endl;
              CDProof* proof = nullptr;
              if (d_data->isProofEnabled())
              {
                proof = d_data->getProof();
                proof->addStep(tlem,
                               PfRule::ARITH_MULT_TANGENT,
                               {},
                               {t,
                                a,
                                b,
                                a_v,
                                b_v,
                                nm->mkConst(Rational(d == 0 ? -1 : 1))});
              }
              d_data->d_im.addPendingLemma(tlem,
                                           InferenceId::ARITH_NL_TANGENT_PLANE,
                                           proof,
                                           asWaitingLemmas);
            }
          }
        }
      }
    }
  }
}

}  // 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		* Gereon Kremer, Andrew Reynolds, 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		* Implementation of tangent_plane check.
14		*/
15
16		#include "theory/arith/nl/ext/tangent_plane_check.h"
17
18		#include "expr/node.h"
19		#include "proof/proof.h"
20		#include "theory/arith/arith_msum.h"
21		#include "theory/arith/inference_manager.h"
22		#include "theory/arith/nl/ext/ext_state.h"
23		#include "theory/arith/nl/nl_model.h"
24		#include "theory/rewriter.h"
25		#include "util/rational.h"
26
27		namespace cvc5 {
28		namespace theory {
29		namespace arith {
30		namespace nl {
31
32	5145	TangentPlaneCheck::TangentPlaneCheck(ExtState* data) : d_data(data) {}
33
34	25	void TangentPlaneCheck::check(bool asWaitingLemmas)
35		{
36	25	Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl;
37	25	NodeManager* nm = NodeManager::currentNM();
38		const std::map<Node, std::vector<Node> >& ccMap =
39	25	d_data->d_mdb.getContainsChildrenMap();
40	25	unsigned kstart = d_data->d_ms_vars.size();
41	90	for (unsigned k = kstart; k < d_data->d_mterms.size(); k++)
42		{
43	100	Node t = d_data->d_mterms[k];
44		// if this term requires a refinement
45	65	if (d_data->d_tplane_refine.find(t) == d_data->d_tplane_refine.end())
46		{
47	30	continue;
48		}
49	70	Trace("nl-ext-tplanes")
50	35	<< "Look at monomial requiring refinement : " << t << std::endl;
51		// get a decomposition
52	35	std::map<Node, std::vector<Node> >::const_iterator it = ccMap.find(t);
53	35	if (it == ccMap.end())
54		{
55		continue;
56		}
57	70	std::map<Node, std::map<Node, bool> > dproc;
58	115	for (unsigned j = 0; j < it->second.size(); j++)
59		{
60	160	Node tc = it->second[j];
61	80	if (tc != d_data->d_one)
62		{
63	90	Node tc_diff = d_data->d_mdb.getContainsDiffNl(tc, t);
64	45	Assert(!tc_diff.isNull());
65	90	Node a = tc < tc_diff ? tc : tc_diff;
66	90	Node b = tc < tc_diff ? tc_diff : tc;
67	45	if (dproc[a].find(b) == dproc[a].end())
68		{
69	35	dproc[a][b] = true;
70	70	Trace("nl-ext-tplanes")
71	35	<< " decomposable into : " << a << " * " << b << std::endl;
72	70	Node a_v_c = d_data->d_model.computeAbstractModelValue(a);
73	70	Node b_v_c = d_data->d_model.computeAbstractModelValue(b);
74		// points we will add tangent planes for
75	70	std::vector<Node> pts[2];
76	35	pts[0].push_back(a_v_c);
77	35	pts[1].push_back(b_v_c);
78		// if previously refined
79	70	bool prevRefine = d_tangent_val_bound[0][a].find(b)
80	105	!= d_tangent_val_bound[0][a].end();
81		// a_min, a_max, b_min, b_max
82	175	for (unsigned p = 0; p < 4; p++)
83		{
84	280	Node curr_v = p <= 1 ? a_v_c : b_v_c;
85	140	if (prevRefine)
86		{
87	80	Node pt_v = d_tangent_val_bound[p][a][b];
88	40	Assert(!pt_v.isNull());
89	40	if (curr_v != pt_v)
90		{
91		Node do_extend = nm->mkNode(
92	80	(p == 1 \|\| p == 3) ? Kind::GT : Kind::LT, curr_v, pt_v);
93	40	do_extend = Rewriter::rewrite(do_extend);
94	40	if (do_extend == d_data->d_true)
95		{
96	60	for (unsigned q = 0; q < 2; q++)
97		{
98	40	pts[p <= 1 ? 0 : 1].push_back(curr_v);
99	80	pts[p <= 1 ? 1 : 0].push_back(
100	40	d_tangent_val_bound[p <= 1 ? 2 + q : q][a][b]);
101		}
102		}
103		}
104		}
105		else
106		{
107	100	d_tangent_val_bound[p][a][b] = curr_v;
108		}
109		}
110
111	110	for (unsigned p = 0; p < pts[0].size(); p++)
112		{
113	150	Node a_v = pts[0][p];
114	150	Node b_v = pts[1][p];
115
116		// tangent plane
117		Node tplane = nm->mkNode(Kind::MINUS,
118	300	nm->mkNode(Kind::PLUS,
119	150	nm->mkNode(Kind::MULT, b_v, a),
120	150	nm->mkNode(Kind::MULT, a_v, b)),
121	300	nm->mkNode(Kind::MULT, a_v, b_v));
122		// construct the following lemmas:
123		// t <= tplane <=> ((a <= a_v ^ b >= b_v) v (a >= a_v ^ b <= b_v))
124		// t >= tplane <=> ((a <= a_v ^ b <= b_v) v (a >= a_v ^ b >= b_v))
125
126	225	for (unsigned d = 0; d < 2; d++)
127		{
128	300	Node b1 = nm->mkNode(d == 0 ? Kind::GEQ : Kind::LEQ, b, b_v);
129	300	Node b2 = nm->mkNode(d == 0 ? Kind::LEQ : Kind::GEQ, b, b_v);
130		Node tlem = nm->mkNode(
131		Kind::EQUAL,
132	300	nm->mkNode(d == 0 ? Kind::LEQ : Kind::GEQ, t, tplane),
133	600	nm->mkNode(
134		Kind::OR,
135	300	nm->mkNode(Kind::AND, nm->mkNode(Kind::LEQ, a, a_v), b1),
136	600	nm->mkNode(
137	900	Kind::AND, nm->mkNode(Kind::GEQ, a, a_v), b2)));
138	300	Trace("nl-ext-tplanes")
139	150	<< "Tangent plane lemma : " << tlem << std::endl;
140	150	CDProof* proof = nullptr;
141	150	if (d_data->isProofEnabled())
142		{
143	26	proof = d_data->getProof();
144	208	proof->addStep(tlem,
145		PfRule::ARITH_MULT_TANGENT,
146		{},
147		{t,
148		a,
149		b,
150		a_v,
151		b_v,
152	208	nm->mkConst(Rational(d == 0 ? -1 : 1))});
153		}
154	150	d_data->d_im.addPendingLemma(tlem,
155		InferenceId::ARITH_NL_TANGENT_PLANE,
156		proof,
157		asWaitingLemmas);
158		}
159		}
160		}
161		}
162		}
163		}
164	25	}
165
166		} // namespace nl
167		} // namespace arith
168		} // namespace theory
169	29340	} // namespace cvc5