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-05-21	Branches:	189	352	53.7 %


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