Head

GCC Code Coverage Report

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